Definitions, theorems, and tactics for boolean type
and standard boolean operators.
Theorems include standard logic ones, as well
as `assert' theorems for converting between boolean
and prop-valued predicates.
This implementation of bool differs from that in Nuprl V3.
There, the booleans were defined as a subtype of the integers.
Here, the use of the Unit + Unit type enables evaluation
of boolean expressions, especially those involving
ifthenelse, using Nuprl's direct computation rules. This
is of great help when these expressions are used in
definitions of recursive functions, whose proof of
well-formedness relies heavily on direct-computation-style
reasoning.